T:Type, as, cs, bs, ds:T List. as @ bs || cs @ ds  as = cs  bs || ds 

latex

Definitions	t  T, l1 || l2, P  Q, x:A. B(x), as @ bs, Prop, False, P & Q, P  Q, ||as||, ij, hd(l), A, AB, tl(l), P  Q
Lemmas	tl wf, ge wf, hd wf, non neg length, length wf1, compat-cons, compat wf, append wf